\begin{tabbing}
$\vdash$  \=$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).\+
\\[0ex]Trans($T$;$x$,$y$.$R$($x$,$y$))
\\[0ex]$\Rightarrow$ \=\{$\forall$$a$, ${\it a'}$, $b$, ${\it b'}$:$T$.\+
\\[0ex]Symmetrize($x$,$y$.$R$($x$,$y$);$a$;$b$) $\Rightarrow$ Symmetrize($x$,$y$.$R$($x$,$y$);${\it a'}$;${\it b'}$) $\Rightarrow$ ($R$($a$,${\it a'}$) $\Leftarrow\!\Rightarrow$ $R$($b$,${\it b'}$))\}
\-\-
\end{tabbing}